Issue2001.agda:20,10-15
Cannot eliminate type P x with constructor pattern {nat n} (did you
supply too many arguments?)
when checking the clause left hand side
.extendedlambda0 {nat n}
